自动化定理证明中的苦涩教训：简单 Agent 循环
🧭 Agent 自反思 + 形式化验证
FAIR at Meta · EPFL · CERMICS, ENPC, Institut Polytechnique de Paris · New York University
提出 h1，一个只靠高效 Lean 接口与验证反馈自反思的简单 agent 循环，在形式定理证明达到 SOTA 并追上复杂工作流
📌 工作参考价值（4 点）
- 构建 LLM agent 做 query 生成、推荐文案或策略搜索时，不要先上规划/多智能体分解；先用单 agent + 可执行验证器（搜索 API 结果、商品约束、SQL 执行）做自反思循环，用 pass@1/多采样衡量，效率和效果常超复杂编排。
- 工具/环境接口的反馈延迟与信息质量是关键：把验证器返回做成结构化、可增量复用（如错误位置、候选修正），减少模型盲目重试；类比 h1 的 Lean 4 增量编译与错误上下文。
- 做消融和 matched-model 对比：换更强模型或更多计算会混淆 workflow 收益；固定模型，对比简单 loop vs 复杂 agent 架构，避免苦涩教训。
- 如果业务里有可靠执行环境（规则校验、线上仿真、评分器），把计算预算花在多次验证反馈循环（test-time compute）上，可能比重构提示/工作流更划算。
ReGE：通过经验合成让 Agent 变得更强
🧭 Agent 经验合成与复用 ★ 深度解读
University of Waterloo · University of North Carolina at Chapel Hill · University of British Columbia
把多次尝试的轨迹与产物联合合成为自包含指导，低 token 成本提升同模型后续执行成功率
📌 工作参考价值（4 点）
- 如果已经在做 agent 或搜索推荐的多路并行采样（例如同一个 query 跑多个策略），别只做投票或 best-of-n；把完整轨迹截断后直接喂给一个 coach 一次性合成“执行计划 + 关键事实 + 失败坑点”，能显著减少指导构建 token（>95%）且保留成功率。
- 工程实现上，截断原始轨迹（steps 120 / reasoning 200 chars / commands 160 chars / artifact 6000 chars）而不预先做 per-trajectory LLM 摘要，可避免独立摘要的信息割裂，Joint synthesis 比 Independent summaries 短约 1/4，总 tokens 降约 20–32%。
- 即使 source 池中都是失败尝试，也能提取可用操作路径（如浏览器任务的打开方式），因此不要丢弃失败的 rollout；mixed 成功/失败池带来的增益最大。
- 低端模型 + ReGE 可达到高端模型同等成功率而成本仅 28%，这为在线服务降本提供了可复用模式：用便宜模型做多次尝试 + 一次性经验合成，替代单次昂贵模型。
思考之前的思考：用元推理扩展智能体推理规模
🧭 Agent 元推理控制与 artifact graph ★ 深度解读
Meta Superintelligence Labs
将 Agent 的控制决策与目标级计算分离，用显式元推理管理 artifact 图、预算和 worker 调度，提升长程任务性能并随预算持续扩展
📌 工作参考价值（4 点）
- 把“控制”与“执行”拆开：在电商推荐/搜索的 Agent 流程中，不要让每个动作都携带完整历史；用轻量 controller state + 可检索 artifact memory，worker 只接收必要 context，能显著降低长上下文信息丢失，提高多步决策稳定性。
- 用 artifact graph 做系统诊断：记录每个中间候选/策略的依赖关系，将失败分解为 coverage（是否产生过正确结果）和 selection（是否选中），类似论文中的覆盖率和 frontier 选择增益，快速定位是召回/生成不足还是最终排序/选择错误。
- 做预算感知的元推理：在线上低延迟场景可以设置 model-call 预算，由 Evaluate 阶段判断剩余预算下每个候选动作的计算价值，小预算时自动关闭深层次控制；论文中低预算 crossover 现象说明元推理 overhead 对简单任务可能有害。
- 引入独立 controller verdict，而非只依赖 worker 自我置信：在推荐 Agent 中对生成结果做独立评估和打分，其排序信号往往比生成模型自报置信度更可靠，可用于最终候选选择。
当智能体减速：通过每 token Elo 分析理解 LLM 智能体的测试时策略
🧭 Agent 测试时计算缩放分析
UC Berkeley · University of Washington · Princeton University · Bespoke Labs
提出 Elo-per-token 分析量化 LLM Agent 测试时计算缩放，发现边际收益递减且拆分并行预算更优
📌 工作参考价值（4 点）
- 对搜索/推荐 Agent 的多步推理或工具调用，可以用 Elo-per-token 曲线监控 token 投入的边际收益，而不是只看最终指标；在边际收益低于独立采样参考线时及时停止或调整策略。
- 独立采样参考线是简单有效的 baseline：如果 Agent 的规划、反思、工具调用不能稳定跑赢重复采样，说明额外复杂度没有带来 token 效率，可考虑简化 Agent 流程或增加采样并行度。
- 利用 scaling inflection point 分配长任务预算：将总 token 预算拆成多个并行 sessions 可能比一个超长 session 获得更高 Elo，对线上高并发 Agent 服务的请求拆分和成本控制有直接指导意义。
- Bradley-Terry 聚合跨任务分数排序的方法可以迁移到电商多指标评估，处理不同 reward 尺度下的成对比较，适合离线评测 Agent 生成物品文案、搜索 query 等开放任务。
超越求解器裁决：用于自动形式化的生成式奖励模型
🧭 Autoformalization · 生成式验证
Case Western Reserve University · Amazon Web Services
将离线 Z3 等价 oracle 蒸馏为生成式连续等价评分，检测 VPU，AUROC 0.961，并带来 11.3 点下游提升
📌 工作参考价值（4 点）
- 把验证器从结构化硬判定升级为连续、参考无关的 reward model：在 query 改写、商品属性约束生成、Agent 工具调用结果校验等场景，训练一个生成式等价性打分器，能捕捉“执行成功但语义偏移”的失败样本，弥补规则/校验器只查语法和返回码的盲区。
- 用离线 oracle 蒸馏低成本验证器：电商/推荐里可用大模型、人工标注或仿真环境构造等价/非等价对，蒸馏到轻量 LM 作为 reward model，再用于线上样本过滤、beam search 重排或 RLHF-style 优化。
- 将连续验证分数用于 agentic test-time compute allocation：对候选生成结果按参考等价性评分动态分配采样/回溯预算，比固定采样或仅按 solver 成功分配更稳；可直接借鉴到多步商品推荐解释、购物 Agent 路径选择。
- 机制分析 trick：通过 decision-projected logit lens / sparse autoencoders 定位 LM 生成中的错误坐标，可用于诊断商品属性约束生成中“哪个 token 维度导致不可满足或不一致”，帮助后续提示或微调。
Twin：用测试时数字孪生玩未知游戏
🧭 测试时世界模型推断与规划 ★ 深度解读
Stanford University · Cornell University · University of Southern California · Yeshiva University
构建可执行世界模型，强制回放验证和规划后执行，以 93.3 分通关 ARC-AGI-3 23/25 个游戏
📌 工作参考价值（4 点）
- 对高成本真实动作（广告投放、push 打扰、人工客服介入）的探索策略，可借鉴 Twin 的 replay validation + halt-on-mismatch：用可执行代码模拟用户/市场动态，每次真实动作前强制模型回放历史交互，不一致就修复；执行中逐步校验，一旦预测失配立即停止并收集 counterexample，避免错误累积放大。
- 把 dynamics 与 goal/reward 显式分离，先验证转移模型，再通过假设-测试循环推断目标。在推荐/搜索中，用户意图常不可见，可先假设当前 session 目标（比价、闲逛、决策），用最小代价提问/推荐验证，而不是等点击或转化 reward 才优化。
- 让 LLM 生成可执行代码作为世界模型，而非黑盒神经网络，获得可解释、可验证、可 BFS 规划的优势；电商 Agent 可让 LLM 写业务规则或用户模拟器，通过离线日志回放验证，再用于策略推演和路径规划。
- 计算成本换真实动作数量：平均每个真实动作 224k tokens，但动作数减少约一半。对高价值动作划算，对高并发低风险推荐不划算；可按动作成本与风险决定是否启用 test-time compute。
GEM：桥接推理与检索的生成式嵌入模型
🧭 生成式嵌入 · 推理增强检索 ★ 深度解读
University of Glasgow
GEM 用单一生成式嵌入模型先对 query 推理再编码，使检索模型能理解推理而不仅是表面匹配，4B 模型超越更大 baseline
📌 工作参考价值（4 点）
- 在搜索 query 理解阶段，可让 retriever 自身生成 query 解析（意图、相关标准、负向条件），再对 query+推理拼接后编码，而非仅依赖原始 query 或外部 query expansion。电商搜索中复杂长尾 query（例如“适合送长辈的安卓手机，不要小米”）可先用 LLM 生成明确检索标准，提升召回精度。
- 训练 embedding 模型时，保留生成能力（联合 causal LM + contrastive loss），用专门 <|embed|> token 而非 EOS token，推理时可复用 KV cache，避免先推理再编码的额外计算；业务部署时可在同一模型内完成 query 推理和向量化，降低 pipeline 延迟。
- 数据合成 trick：采样多个 reasoning 候选，用 LLM 判断原始相关文档是否仍满足该推理来过滤；再基于通过过滤的推理生成正文档和“主题相似但违背某个推理标准”的 hard negatives。这种对齐数据能显著提升 embedding 对指令/约束的敏感度，适用于电商推荐中“可解释偏好”或“多条件过滤”场景。
- 测试期 compute scaling：通过 prompt 要求生成更长推理（如目标词数）可稳定提升 nDCG，但到 1024 词后饱和；工程上可对高价值 query 分层使用，长尾复杂 query 用扩展推理，普通 query 短推理，平衡效果与成本。
选择性验证：预算感知的推理分配方法
🧭 推理时计算资源分配优化
Department of Computer Science, Virginia Tech · Fralin Biomedical Research Institute, Virginia Tech · FBRI Cancer Research Center, Washington, DC
SEVRA用门控机制选择性触发验证，在提升准确率的同时大幅削减后生成token开销
📌 工作参考价值（4 点）
- 选择性验证降低服务成本：在推荐Agent或RAG管线中，对LLM生成的解释、候选理由进行二次验证会增加延迟和费用，可训练轻量门控模型（基于初始输出的隐含状态或置信度特征）决定是否触发验证，避免全量验证，参考SEVRA将验证token减少26.8%~91.2%的收益。
- 优先扩展初始推理预算：实验表明延长初始生成（如增加token限制）往往比事后验证更高效，在推荐场景中，若已为LLM分配推理预算，应优先投入在首次生成更长、更细致的推理链，而非立即增加验证步骤。
- 门控模型可跨任务迁移：SEVRA的门控策略从数学任务直接迁移到常识推理无需重训，仍能保持高精度且大幅减少验证调用，暗示在领域迁移时，基于求解器状态的“可恢复性”特征具通用性，可尝试复用于搜索词推荐、文案生成等不同任务的验证控制。
- 显式控制有害翻转：对于高敏感场景（如电商价格推荐、法律合规审查），SEVRA将有危害性答案翻转率从2.2%降至1.0%，这种“先判定再验证”的思路可用于拦截LLM在二次推理时可能引入的错误修改，提升输出稳定性。